Nuprl Lemma : subtype_rel-deq
11,40
postcript
pdf
A
,
B
:Type. (
A
r
B
)
(
x
,
y
:
A
. (
x
=
y
B
)
(
x
=
y
))
(EqDecider(
B
)
r EqDecider(
A
))
latex
Definitions
x
:
A
.
B
(
x
)
,
P
Q
,
t
T
,
,
S
T
Lemmas
subtype-deq
,
deq
wf
origin
A, B:Type. (A 
r B) 
(x, y:A. (x = y 
B) (x = y)) (EqDecider(B) r EqDecider(A)) A, B:Type. (A r B) (x, y:A. (x = y B) (x = y)) (EqDecider(B) r EqDecider(A)) x:A. B(x) Q T
T